| Definitions |  T, A c B,  x:A. B(x), rcv(l,tg), P  Q, i <z j,   b, i  z j, nth_tl(n;as), hd(l), i j < k, ||as||, {i..j }, l[i], {T}, SQType(T), P & Q, Top,  , True, if b then t else f fi , Y, reduce(f;k;as), deq-member(eq;x;L), tt, ff, t.1,  ,   x. t(x), t  T, MaName, R-names(A), R-loc(R), Rda(R), x dom(f), Rnone?(x1), Rplus?(x1),  b, P   Q, Knd,  x:A. B(x), outl(x), t.2, isl(x), tag(k), isrcv(k), Dec(P), P  Q, P Q, False, x(s), Unit, A, Realizer, locl(a), Rrframe(loc;x;L), Rbframe(loc;k;L), Raframe(loc;k;L), Rpre(loc;ds;a;p;P), Rsends(ds;knd;T;l;dt;g), Reffect(loc;ds;knd;T;x;f), Rsframe(lnk;tag;L), Rframe(loc;T;x;L), Rinit(loc;T;x;v), left  right, Rnone(),  , fpf-domain(f) |